'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(a()) -> g(h(a())) , h(g(x)) -> g(h(f(x))) , k(x, h(x), a()) -> h(x) , k(f(x), y, x) -> f(x)} Details: We have computed the following set of weak (innermost) dependency pairs: { f^#(a()) -> c_0(h^#(a())) , h^#(g(x)) -> c_1(h^#(f(x))) , k^#(x, h(x), a()) -> c_2(h^#(x)) , k^#(f(x), y, x) -> c_3(f^#(x))} The usable rules are: { f(a()) -> g(h(a())) , h(g(x)) -> g(h(f(x)))} The estimated dependency graph contains the following edges: {h^#(g(x)) -> c_1(h^#(f(x)))} ==> {h^#(g(x)) -> c_1(h^#(f(x)))} {k^#(x, h(x), a()) -> c_2(h^#(x))} ==> {h^#(g(x)) -> c_1(h^#(f(x)))} {k^#(f(x), y, x) -> c_3(f^#(x))} ==> {f^#(a()) -> c_0(h^#(a()))} We consider the following path(s): 1) { k^#(x, h(x), a()) -> c_2(h^#(x)) , h^#(g(x)) -> c_1(h^#(f(x)))} The usable rules for this path are the following: { f(a()) -> g(h(a())) , h(g(x)) -> g(h(f(x)))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(a()) -> g(h(a())) , h(g(x)) -> g(h(f(x))) , k^#(x, h(x), a()) -> c_2(h^#(x)) , h^#(g(x)) -> c_1(h^#(f(x)))} Details: We apply the weight gap principle, strictly orienting the rules {k^#(x, h(x), a()) -> c_2(h^#(x))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {k^#(x, h(x), a()) -> c_2(h^#(x))} Details: Interpretation Functions: f(x1) = [1] x1 + [1] a() = [0] g(x1) = [1] x1 + [1] h(x1) = [1] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] h^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [0] k^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {h^#(g(x)) -> c_1(h^#(f(x)))} and weakly orienting the rules {k^#(x, h(x), a()) -> c_2(h^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {h^#(g(x)) -> c_1(h^#(f(x)))} Details: Interpretation Functions: f(x1) = [1] x1 + [1] a() = [0] g(x1) = [1] x1 + [9] h(x1) = [1] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] h^#(x1) = [1] x1 + [0] c_1(x1) = [1] x1 + [4] k^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(a()) -> g(h(a())) , h(g(x)) -> g(h(f(x)))} Weak Rules: { h^#(g(x)) -> c_1(h^#(f(x))) , k^#(x, h(x), a()) -> c_2(h^#(x))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { f(a()) -> g(h(a())) , h(g(x)) -> g(h(f(x)))} Weak Rules: { h^#(g(x)) -> c_1(h^#(f(x))) , k^#(x, h(x), a()) -> c_2(h^#(x))} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { f_0(2) -> 12 , f_0(3) -> 12 , f_1(2) -> 16 , f_1(3) -> 16 , f_1(13) -> 18 , a_0() -> 2 , a_1() -> 14 , g_0(2) -> 3 , g_0(3) -> 3 , g_1(13) -> 12 , g_1(13) -> 16 , h_1(14) -> 13 , h^#_0(2) -> 8 , h^#_0(3) -> 8 , h^#_0(12) -> 11 , h^#_1(16) -> 15 , h^#_1(18) -> 17 , c_1_0(11) -> 8 , c_1_1(15) -> 8 , c_1_1(17) -> 11 , c_1_1(17) -> 15 , k^#_0(2, 2, 2) -> 10 , k^#_0(2, 2, 3) -> 10 , k^#_0(2, 3, 2) -> 10 , k^#_0(2, 3, 3) -> 10 , k^#_0(3, 2, 2) -> 10 , k^#_0(3, 2, 3) -> 10 , k^#_0(3, 3, 2) -> 10 , k^#_0(3, 3, 3) -> 10} 2) { k^#(f(x), y, x) -> c_3(f^#(x)) , f^#(a()) -> c_0(h^#(a()))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: f(x1) = [0] x1 + [0] a() = [0] g(x1) = [0] x1 + [0] h(x1) = [0] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] h^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] k^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {f^#(a()) -> c_0(h^#(a()))} Weak Rules: {k^#(f(x), y, x) -> c_3(f^#(x))} Details: We apply the weight gap principle, strictly orienting the rules {f^#(a()) -> c_0(h^#(a()))} and weakly orienting the rules {k^#(f(x), y, x) -> c_3(f^#(x))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(a()) -> c_0(h^#(a()))} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a() = [0] g(x1) = [0] x1 + [0] h(x1) = [0] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [1] x1 + [1] c_0(x1) = [1] x1 + [0] h^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] k^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { f^#(a()) -> c_0(h^#(a())) , k^#(f(x), y, x) -> c_3(f^#(x))} Details: The given problem does not contain any strict rules 3) {k^#(x, h(x), a()) -> c_2(h^#(x))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: f(x1) = [0] x1 + [0] a() = [0] g(x1) = [0] x1 + [0] h(x1) = [0] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] h^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] k^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {k^#(x, h(x), a()) -> c_2(h^#(x))} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {k^#(x, h(x), a()) -> c_2(h^#(x))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {k^#(x, h(x), a()) -> c_2(h^#(x))} Details: Interpretation Functions: f(x1) = [0] x1 + [0] a() = [0] g(x1) = [0] x1 + [0] h(x1) = [1] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] h^#(x1) = [1] x1 + [0] c_1(x1) = [0] x1 + [0] k^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {k^#(x, h(x), a()) -> c_2(h^#(x))} Details: The given problem does not contain any strict rules 4) {k^#(f(x), y, x) -> c_3(f^#(x))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: f(x1) = [0] x1 + [0] a() = [0] g(x1) = [0] x1 + [0] h(x1) = [0] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [0] x1 + [0] c_0(x1) = [0] x1 + [0] h^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] k^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {k^#(f(x), y, x) -> c_3(f^#(x))} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {k^#(f(x), y, x) -> c_3(f^#(x))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {k^#(f(x), y, x) -> c_3(f^#(x))} Details: Interpretation Functions: f(x1) = [1] x1 + [0] a() = [0] g(x1) = [0] x1 + [0] h(x1) = [0] x1 + [0] k(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] f^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] h^#(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] k^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {k^#(f(x), y, x) -> c_3(f^#(x))} Details: The given problem does not contain any strict rules